\chapter{Minimizzazione}
\label{cap:cap_3}
Fina ad ora abbiamo definito un linguaggio per i contratti BPEL, un predicato di terminazione con successo e un sistema di transizioni su tale linguaggio. Abbiamo poi formalizzato e rappresentato graficamente gli automi corrispondenti ad ogni costrutto dei contratti, chiamati Automi Comportamentali, sulla base dei tre concetti enunciati precedentemente. A questo punto risulta di particolare importanza, per il raggiungimento dei nostri obiettivi, sviluppare una fase di minimizzazione da applicare ai nostri AC. Inizialmente terremo in considerazione le tecniche classiche di minimizzazione per valutare se sono attendibili e veritiere anche nei nostri tipi di automi.
\begin{example}
\label{ex:min}   
In \figurename~\ref{fig:rnf_A} viene mostrato l'automa corrispondente all'attivit\`a $(\co a \oplus \co b)+(\co a \oplus \co c)$. Possiamo evincere dalla \tablename~\ref{tab:minimizzazione1} che l'applicazione delle tecniche classiche di minimizzazione marca tutte le coppie di stati come distinguibili, poich\'e esistono clienti che sono soddisfatti (vedi Definizione~\ref{def:cliente_sodd}) di interagire con uno stato ma non sono altrettanto soddisfatti di interagire con un altro, considerazione valida per tutte le coppie di stati.\\\\
\begin{table}[h]
\centering
\begin{tabular}{l|c|c|c|c|c|c|c|c|c|}
\cline{1-0} \cline{2-1}
$q_1$ & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2}
$q_2$ & \ding{55} & \ding{55} \\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3}
$q_3$ & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} 
$q_4$ & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} \cline{6-5}
$q_5$ & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} \cline{6-5} \cline{7-6} 
$q_6$ & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} \cline{6-5} \cline{7-6} \cline{8-7} 
$q_7$ & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} \cline{6-5} \cline{7-6} \cline{8-7} \cline{9-8}
$q_8$ & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3} \cline{5-4} \cline{6-5} \cline{7-6} \cline{8-7} \cline{9-8} \cline{10-9}
$q_9$ & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55} & \ding{55}\\
\hline
 & $q_0$ & $q_1$ & $q_2$ & $q_3$ & $q_4$ & $q_5$ & $q_6$ & $q_7$ & $q_8$\\
\end{tabular}
\caption{Ricerca degli stati distinguibili dell'AC in \figurename~\ref{fig:rnf_A}}
\label{tab:minimizzazione1}
\end{table}

Per fare un esempio partiamo dalla definizione di cliente soddisfatto e prendiamo in considerazione due stati qualunque $q_1, q_3$ appartenenti all'AC in \figurename~\ref{fig:rnf_A}. Dato un cliente $c$, se $c \scomp q_1$ sar\`a, considerando tutte le interazioni, $c\not\scomp q_3$ e viceversa. La motivazione \`e che prendendo una transizione dello stato $q_1$ posso raggiungere lo stato $q_5$, che ha disponibili le azioni $\{\co a,\co c\}$ delle quali non posso disporre seguendo qualunque transizione da $q_3$. Ovviamente \`e una cosiderazione valida per tutte le coppie di stati dell'AC in \figurename~\ref{fig:rnf_A}.  
\begin{figure}[h]
  \centering
    \includegraphics{examples/rnf.A.eps}
  \caption{AC dell'attivit\`a $(\co a \oplus \co b)+(\co a \oplus \co c)$}
  \label{fig:rnf_A}
\end{figure}
\end{example}
L'esistenza di un AC (vedi \figurename~\ref{fig:rnf_B1}) equivalente a quello in \figurename~\ref{fig:rnf_A} con un numero minore di stati dimostra la non veridicit\`a dei risultati nell'applicare la teoria di minimizzazione classica ai nostri AC. Quindi quest'ultima non essendo (per costruzione dei nostri AC) praticabile, diventa di fondamentale importanza l'introduzione di una forma normale per i nostri automi. Introduciamo questo concetto non per dare una struttura diversa agli AC, ma bens\`i per normalizzarli in modo da rendere attendibile l'applicazione dell'algoritmo per la ricerca degli stati distinguibili sui nostri automi, altrimenti come visto in precedenza in alcuni casi l'automa risulterebbe minimo anche se in realt\`a non lo sarebbe. Partiamo dalla definizione classica di forma normale (vedi \cite{Laneve_Padovani-07}), affermando che ogni contratto pu\`o essere riscritto in uno equivalente il cui comportamento \`e in forma normale. L'idea fondamentale di questa forma \`e che saturando l'isieme di "`"`azioni"'"' di un comportamento il suo significato non cambia. Questa definizione per quanto riguarda i nostri AC non \`e ottimale, nel senso che il problema di questa forma normale, come sempre, \`e quello di creare un'esplosione nel numero di stati rispetto all'automa originale. Per far fronte a ci\`o cerchiamo una forma normale pi\`u "`"`economica"'"' che ci produca un automa pi\`u piccolo (in numero di stati) rispetto a quello risultate dalla forma normale classica. Quindi nel proseguio vedremo come definire la nostra forma normale dando una definizione piu formale ed "`"`economica"'"', poi una volta costruito l'automa in forma normale ci applicheremo le tecniche classiche di minimizzazione.
\begin{figure}[h]
  \centering
    \includegraphics{examples/rnf.B.eps}
  \caption{AC equivalente all'AC dell'attivit\`a $(\co a \oplus \co b)+(\co a \oplus \co c)$}
  \label{fig:rnf_B1}
\end{figure}
 
\section{Acceptance set}
Prima di formalizzare il concetto di forma normale diamo le definizioni di \emph{ready set} e \emph{acceptance set} che ci ritorneranno utili nel proseguio della tesi. Usiamo $\rset{r},\rset{s},\dots$ per indicare \emph{ready set} di uno stato, definiti nella Notazione~\ref{not:int_c-s} con la dicitura $S(q)$, che andremo a calcolare sugli stati stabili e $\mathcal{A},\mathcal{B},\dots$ per indicare \emph{acceptance set} che andremo a calcolare sugli stati non stabili e quindi aventi tutte trasizioni del tipo $\lred{\tau}$ oppure $\lred{\tau}$ e $\lred{\alpha}$. Queste due diciture tengono traccia delle azioni visibili di un comportamento evitando, per costruzione degli AC, perdite di informazione nel contratto. Vedremo anche i formalismi di saturazione e caratterizzazione di un \emph{acceptance set} che utilizzeremo nella costruzione della nostra forma normale. 

\begin{notation}
\label{not:aset}

\[
  \mathcal{A}(P) \eqdef \{ S(q) \mid q \in \stable(P) \}
\]
\end{notation}

\begin{definition}[Acceptance set saturato]
\label{def:asat}
L'\emph{acceptance set saturato} di $\mathcal{A}$ \`e l'acceptance set
\[
\textstyle
  \asat{\mathcal{A}} \eqdef
  \{
%  \rset{r}\subseteq\bigcup_{\rset{r}''\in\mathcal{A}}\rset{r}''
  \rset{r}\subseteq\bigcup_{\rset{r}\in\mathcal{A}}\rset{r}
  \mid \exists \rset{s}\in\mathcal{A}:
  \rset{s}\subseteq\rset{r}
  \}
\]
\end{definition}

In altri termini $\asat{\mathcal{A}}$ \`e il pi\`u piccolo acceptance
set convesso e chiuso per unione che contiene $\mathcal{A}$. Infatti
\begin{itemize}
\item se $\rset{r},\rset{r}'\in\asat{\mathcal{A}}$, allora
  $\rset{r}\cup\rset{r}'\in\asat{\mathcal{A}}$;

\item se $\rset{r} \subseteq \rset{r}' \subseteq \rset{r}''$ e
  $\rset{r},\rset{r}''\in\asat{\mathcal{A}}$, allora
  $\rset{r}'\in\asat{\mathcal{A}}$.
\end{itemize}

\begin{definition}[Acceptance set minimo]
\label{def:amin}
Il \emph{minimo acceptance set} di $\mathcal{A}$ \`e l'acceptance set
\[
  \amin{\mathcal{A}} \eqdef \{ \rset{r} \in \mathcal{A} \mid \nexists
  \rset{s}\in\mathcal{A} \setminus \{\rset{r}\}:
  \rset{s}\subseteq\rset{r}\}
\]
\end{definition}

\begin{proposition}
$\amin{\mathcal{A}} \subseteq \mathcal{A} \subseteq
  \asat{\mathcal{A}}$.
\end{proposition}

\begin{definition}[Acceptance set caratteristico]
\label{def:acar}
L'\emph{acceptance set caratteristico} di $\mathcal{A}$, denotato da
$\acar{\mathcal{A}}$, \`e l'acceptance set
\[
  \acar{\mathcal{A}} \eqdef
  \left\{
  \begin{array}{@{}l@{\qquad}l}
    \amin{\mathcal{A}}
    & \text{se $\bigcup_{\rset{r}\in\mathcal{A}} \rset{r} = \bigcup_{\rset{r}\in\amin{\mathcal{A}}} \rset{r}$} \\
    \amin{\mathcal{A}} \cup \{ \bigcup_{\rset{r}\in\mathcal{A}} \rset{r}\}
    & \text{altrimenti}
  \end{array}
  \right.
\]
\end{definition}

L'acceptance set caratteristico di $\mathcal{A}$ \`e l'acceptance set
\emph{pi\`u piccolo} (con il minor numero di ready set) tale che
$\asat{\acar{\mathcal{A}}} = \asat{\mathcal{A}}$.

\begin{example}
Attraverso l'automa in \figurename~\ref{fig:aset}, corrispondente al servizio $\co a \oplus (\co a + (\co b \oplus \co c))$, diamo un riscontro pratico alle definizioni sopra citate. Dati:

\begin{itemize}
\item $S(q_5)=\{\emptyset\}$;
\item $S(q_4)=\{\overline a,\overline c\}$;
\item $S(q_3)=\{\overline a,\overline b\}$;
\item $S(q_1)=\{\overline a\}$;
\item $\mathcal{A}(\{q_2\})=\{\{\overline a,\overline b\}, \{\overline a,\overline c\}\}$;
\end{itemize}
e l'\emph{acceptance set} dello stato iniziale $\mathcal{A}(\{q_0\})=\{\{a\},\{a,c\},\{a,b\}\}$, avremo che:
\begin{itemize}
\item $\asat{\mathcal{A}}(\{q_0\}) = \{\{a\},\{a,c\},\{a,b\},\{a,b,c\}\}$;
\item $\amin{\mathcal{A}}(\{q_0\}) = \{a\}$;
\item $\acar{\mathcal{A}}(\{q_0\}) = \{\{a\},\{a,b,c\}\}$.
\end{itemize}
\end{example}

\begin{figure}[h]
  \centering
    \includegraphics[height=8.4cm]{examples/a_set.A.eps}
  \caption{AC dell'attivit\`a $\co a \oplus (\co a + (\co b \oplus \co c))$}
  \label{fig:aset}
\end{figure}

\newpage
\begin{theorem}
\label{th:mineq}
Le seguenti affermazioni sono equivalenti:
\begin{enumerate}
\item per ogni $\rset{r}\in\mathcal{A}$ esiste
  $\rset{s}\in\mathcal{B}$ tale che $\rset{s}\subseteq\rset{r}$ e per
  ogni $\rset{s}\in\mathcal{B}$ esiste $\rset{r}\in\mathcal{A}$ tale
  che $\rset{r}\subseteq\rset{s}$;

\item $\amin{\mathcal{A}} = \amin{\mathcal{B}}$.
\end{enumerate}
\begin{proof}
($1 \Rightarrow 2$) Sia $\rset{r} \in \amin{\mathcal{A}}$. Allora
  $\rset{r} \in \mathcal{A}$ e per ipotesi esiste $\rset{s} \in
  \mathcal{B}$ tale che $\rset{s} \subseteq \rset{r}$. Ancora per
  ipotesi, esiste $\rset{r}' \in \mathcal{A}$ tale che $\rset{r}'
  \subseteq \rset{s} \subseteq \rset{r}$. Siccome $\rset{r} \in
  \amin{\mathcal{A}}$, deve essere $\rset{r}' = \rset{s} = \rset{r}$,
  ovvero $\rset{r} \in \mathcal{B}$. Supponiamo per assurdo che
  $\rset{r} \not\in \amin{\mathcal{B}}$. Allora esiste $\rset{s}' \in
  \mathcal{B}$ tale che $\rset{s}' \subsetneq \rset{r}$. Per ipotesi
  deve esistere $\rset{r}'' \in \mathcal{A}$ tale che
  $\rset{r}''\subseteq\rset{s}'\subsetneq\rset{r}$, ma questo \`e
  assurdo perch\'e $\rset{r} \in \amin{\mathcal{A}}$. Concludiamo che
  $\amin{\mathcal{A}} \subseteq \amin{\mathcal{B}}$ e la tesi segue
  per simmetria.

($2 \Rightarrow 1$) Sia $\rset{r} \in \mathcal{A}$. Allora esiste
  $\rset{s}\in\amin{\mathcal{A}}$ tale che
  $\rset{s}\subseteq\rset{r}$. Per ipotesi
  $\rset{s}\in\amin{\mathcal{B}}\subseteq\mathcal{B}$. La tesi segue
  per simmetria.
\end{proof}
\end{theorem}

\iffalse
($\amin\mathcal{A} = \amin\mathcal{B}$) Supponiamo per assurdo che non valga l'equivalenza 
tra ~\ref{it:1} e ~\ref{it:3} e quindi per ogni $\rset{r}\in \mathcal{A}$ esiste un $\rset{s}\in \mathcal{B}$ tale che 
$\rset{s}\nsubseteq\rset{r}$, o viceversa ; che \`e equivalente 
a $\amin\mathcal{A} = \amin\mathcal{B}$. Cadiamo subito nell'assurdo poich\'e non potr\`a essere
per Definizione~\ref{def:amin} che $\amin\mathcal{A} = \amin\mathcal{B}$.

($\acar\mathcal{A} = \acar\mathcal{B}$) Possiamo notare semplicemente che se $\amin\mathcal{A} = \amin\mathcal{B}$ allora per la Definizione~\ref{def:acar} anche  $\acar\mathcal{A} = \acar\mathcal{B}$.

($\asat\mathcal{A} = \asat\mathcal{B}$) Dalla Definzione~\ref{def:acar} notiamo che se $\acar\mathcal{A} = \acar\mathcal{B}$
 $\asat\acar\mathcal{A} = \asat\mathcal{A}$ da cui \`e facile concludere dicendo che $\asat\mathcal{A}=\asat\mathcal{B}$.
\fi

\begin{theorem}
\label{th:satcarmineq}
Siano $\mathcal{A}$ e $\mathcal{B}$ acceptance set tali che
$\bigcup\mathcal{A} = \bigcup\mathcal{B}$.
Le seguenti affermazioni sono equivalenti:
\begin{enumerate}
\item $\amin{\mathcal{A}}=\amin{\mathcal{B}}$;

\item $\acar{\mathcal{A}} = \acar{\mathcal{B}}$;

\item $\asat{\mathcal{A}} = \asat{\mathcal{B}}$.
\end{enumerate}
\end{theorem}
\begin{proof}
($1 \Rightarrow 2$) Ovvio per definizione di $\acar{\mathcal{A}}$ e
  $\acar{\mathcal{B}}$.

($2 \Rightarrow 3$) Ovvio in quanto $\asat{\mathcal{A}} =
  \asat{\acar{\mathcal{A}}} = \asat{\acar{\mathcal{B}}} =
  \asat{\mathcal{B}}$ per le propriet\`a di $\acar{\mathcal{A}}$ e
  $\acar{\mathcal{B}}$.

($3 \Rightarrow 1$) Sia $\rset{r} \in \amin{\mathcal{A}} \subseteq
  \asat{\mathcal{A}} = \asat{\mathcal{B}}$. Allora esiste $\rset{s}
  \in \amin{\mathcal{B}}$ tale che $\rset{s} \subseteq
  \rset{r}$. Supponiamo per assurdo che $\rset{s} \subsetneq
  \rset{r}$. Allora $\rset{s} \in \amin{\mathcal{B}} \subseteq
  \asat{\mathcal{B}} = \asat{\mathcal{A}}$, ovvero esiste $\rset{r}'
  \in \mathcal{A}$ tale che $\rset{r}'\subseteq \rset{s} \subsetneq
  \rset{r}$, ma questo \`e assurdo dal momento che $\rset{r} \in
  \amin{\mathcal{A}}$. Concludiamo che $\amin{\mathcal{A}} \subseteq
  \amin{\mathcal{B}}$ e la tesi segue per simmetria.
\end{proof}

\begin{proposition}
Sia $\mathcal{B}$ un acceptance set tale che $\asat{\mathcal{A}} =
\asat{\mathcal{B}}$, allora $|\acar{\mathcal{A}}| \leq |\mathcal{B}|$.
\end{proposition}
\begin{proof}
Supponiamo per assurdo che esista un acceptance set $\mathcal{B}$ tale
che $\asat{\mathcal{A}} = \asat{\mathcal{B}}$ e $|\mathcal{B}| <
|\acar{\mathcal{A}}|$. Dal Teorema~\ref{th:mineq} abbiamo che
$\amin{\mathcal{A}} = \amin{\mathcal{B}}$.  Ragionando per casi sulla
definizione di $\acar{\mathcal{A}}$ abbiamo due possibilit\`a.  Se
$\bigcup_{\rset{r}\in\mathcal{A}} \rset{r} =
\bigcup_{\rset{r}\in\amin{\mathcal{A}}} \rset{r}$, allora
$\acar{\mathcal{A}} = \amin{\mathcal{A}} = \amin{\mathcal{B}}$, dunque
$|\mathcal{B}| < |\acar{\mathcal{A}}| = |\amin{\mathcal{B}}|$ e questo
\`e assurdo dal momento che $|\amin{\mathcal{B}}| \leq |\mathcal{B}|$
per definizione di $\amin{\mathcal{B}}$.  Se
$\bigcup_{\rset{r}\in\amin{\mathcal{A}}} \rset{r} \subsetneq
\bigcup_{\rset{r}\in\mathcal{A}} \rset{r}$, allora $\acar{\mathcal{A}}
= \amin{\mathcal{A}} \cup \{\bigcup_{\rset{r}\in\mathcal{A}}
\rset{r}\}$, dunque $|\mathcal{B}| < |\amin{\mathcal{A}}| + 1 =
|\amin{\mathcal{B}}| + 1$ da cui deriviamo
$|\mathcal{B}|\leq|\amin{\mathcal{B}}|$. Per definizione di
$\amin{\mathcal{B}}$ abbiamo che
$\amin{\mathcal{B}}\subseteq\mathcal{B}$, dunque deve essere
$|\mathcal{B}|=|\amin{\mathcal{B}}|$ ovvero
$\mathcal{B}=\amin{\mathcal{B}} = \amin{\mathcal{A}}$. Da
$\bigcup_{\rset{r}\in\amin{\mathcal{A}}} \rset{r} \subsetneq
\bigcup_{\rset{r}\in\mathcal{A}} \rset{r}$ otteniamo
$\bigcup_{\rset{s}\in\mathcal{B}} \rset{s} \subsetneq
\bigcup_{\rset{r}\in\mathcal{A}} \rset{r}$, ma questo contraddice
l'ipotesi $\asat{\mathcal{A}} = \asat{\mathcal{B}}$.
\end{proof}

\section{Forma normale ridotta}
Introduciamo ora il concetto di \emph{forma normale ridotta} che ci permette di riscrivere ogni contratto in uno equivalente la cui attivit\`a \`e in forma normale. L'idea di base \`e che l'insieme dei ready set di un'attivit\`a, quindi il suo acceptance set, possono essere saturati (acceptance set saturo) senza cambiare il significato del comportamento. Per esempio $a \oplus b \eqc a \oplus b \oplus (a+b)$ dove, per definizione di $\asat\mathcal{A}$, la prima attivit\`a ha $\mathcal{A}=\{\{a\},\{b\}\}$, mentre la seconda ha $\mathcal{A}=\{\{a\},\{b\},\{a,b\}\}$. La motivazione per cui la definiamo \emph{ridotta} \`e che nella nostra ricerca invece di utilizzare la saturazione degli accenptance set, prendiamo in considerazione l'acceptance set caratteristico di un'attivit\`a che per definizione di $\acar\mathcal{A}$ e di $\amin\mathcal{A}$ \`e, appunto, ridotto rispetto a quello saturo. Il fatto di utilizzare l'acceptance set caratteristico non toglie semantica all'attivit\`a trasformata in forma normale ridotta.
%In \figurename~\ref{fig:rnf_A} viene mostrato l'automa corrispondente all'attivit\`a $(a \oplus b)+(a \oplus c)$. Questo esempio motiva, in parte, l'utilizzo della forma normale ridotta in quanto prendendo come riferimento gli stati: $q_2, q_4$ possiamo affermare che, per definizione di cliente soddisfatto, non esiste un cliente che li distingua in quanto: sia $p$ lo stato di un cliente avremo che $p \scomp q$ dove $q\in\{q_2, q_4\}$, se ogni interazione massimale finita $p_0 \parop q_0 \wlred{} p_n \parop q_n$ di $p$ e $q$ \`e tale che $p_n$ \`e finale. Siccome indichiamo con $\wlred{}$ la chiusura riflessiva e transitiva della relazione $\lred{}$ tra le coppie di stati, possiamo facilmente concludere che le interazioni massimali finite terminano nello stesso stato $q_7$, giustificando l'equivalenza degli stati.
%Riporteremo lo stesso esempio per dimostrare l'utilit\`a di trasformare un'automa in forma normale ridotta, in quanto ci permetter\`a di eliminare l'equivalenze sopra citate, poi una volta spiegato l'algoritmo per la ricerca degli stati distinguibili mostreremo come senza il passaggio tramite la forma normale ridotta tale algoritmo non sarebbe veritiero e attendibile.

\subsection{Definizione di automa in forma normale ridotta}

Un automa $N$ \`e in forma normale ridotta, se ogni stato $q\in Q_N$:
\begin{itemize}
\item ha tutte transizioni del tipo $q \lred{\alpha}$ oppure tutte transizioni del tipo $q \lred{\tau}$;
%\item se ha due o piu transizioni $q \lred{a},q \lred{a_1},..., q \lred{a_n}$ con $a,a_1,...,a_n\in\alpha$, significa che $a\neq a_1\neq...\neq a_n$.
\item se ha due o pi\`u transizioni $q \lred{\alpha} q', q \lred{\alpha} q''$, con $\alpha\in\Sigma$ allora $q' = q''$;
\item se ha due o pi\`u transizioni $q \lred{\tau}$, significa che $q$ ha rispettivamente due o pi\`u $\rset{r}\in\acar{\mathcal{A}(\{q\})}$, pioch\'e per ogni $\rset{r}$ viene associata una transizione $q \lred{\tau}q'$ dove $q'$ ha come acceptance set il ready-set $\rset{r}$. 
\end{itemize}
Partendo dall'Automa Comportamentale originale costruiamo il rispettivo AC in forma normale ridotta. La struttura degli stati in questa forma cambia, in quanto a dispetto di prima lo stato contiene internamente anche informazioni sul suo acceptance set caratteristico.\\

Dato un automa
\[
  M \eqdef (Q, \Sigma, \delta, q, F)
\]
definiamo
\[
  N = (2^Q \times 2^{2^\Sigma}, \Sigma, \delta', (\{q\}, \acar{\mathcal{A}(\{q\})}), F)
\]
dove $\delta'$ \`e la pi\`u piccola funzione di transizione tale che
\[
\begin{array}{rcl@{\qquad}l}
  \delta'((P, \mathcal{A}), \tau) & = & \bigcup_{\rset{r}\in\mathcal{A}} \{ (P, \{\rset{r}\})\}
  & \text{se $|\mathcal{A}| > 1$}
  \\
  \delta'((P, \{\rset{r}\}), \alpha) & = & \{ (P(\alpha), \acar{\mathcal{A}(P(\alpha))})\}
  & \alpha \in \rset{r}
\end{array}
\]

\begin{theorem}
Sia $q$ lo stato iniziale di un automa $M$ e sia $q'$ lo stato
iniziale dell'automa $\rnf(M)$. Allora $q \eqc q'$.
\end{theorem}
\begin{proof}
Ci limitiamo a considerare la condizione $q \subc q'$. La
dimostrazione di $q' \subc q$ \`e del tutto analoga. Per dimostrare $q
\subc q'$ \`e sufficiente dimostrare che la relazione
\[
  {\rel{R}} \eqdef \{ (\{q\}(s), \{(\{q\}(s), \acar{\mathcal{A}(\{q\}(s))})\} \mid q \wlred{s} \}
\]
\`e un sottoservizio coinduttivo. Sia $(P,Q)\in{\rel{R}}$. Allora
esiste $s$ tale che
\[
  q \wlred{s}
  \text{\quad e\quad}
  P = \{q\}(s)
  \text{\quad e\quad}
  Q = \{(P, \acar{\mathcal{A}(P)})\}
  \,.
\]

Per quanto riguarda la condizione~(1) della
Definizione~\ref{def:subccoind}, osserviamo che $\mathcal{A}(Q) =
\acar{\mathcal{A}(P)}$ per costruzione dell'automa in forma normale
ridotta. Quindi $\asat{\mathcal{A}(Q)} = \asat{\acar{\mathcal{A}(P)}}
= \asat{\mathcal{A}(P)}$ per definizione di $\acar{\mathcal{A}(P)}$ da
cui deduciamo, per il Teorema~\ref{th:satcarmineq}, che
$\amin{\mathcal{A}(P)} = \amin{\mathcal{A}(Q)}$.  Dato
$p\in\stable(Q)$ abbiamo che $S(p) \in \mathcal{A}(Q)$.  Per il
Teorema~\ref{th:mineq}, esiste $\rset{r} \in \mathcal{A}(P)$ tale
che $\rset{r} \subseteq S(p)$, ovvero esiste $p'\in\stable(P)$ tale
che $S(p') \subseteq S(p)$.

Per quanto riguarda la condizione~(2) della
Definizione~\ref{def:subccoind}, supponiamo che esista $p\in Q$ tale
che $p \wlred{\alpha}$. Dunque esiste $\rset{r}\in\acar{\mathcal{A}(P)}$
tale che $\alpha\in\rset{r}$, ovvero esiste $\rset{r}'\in\mathcal{A}(P)$
tale che $\alpha\in\rset{r}'$. Per definizione di $\mathcal{A}(P)$, esiste
$p'\in\stable(P)$ tale che $\alpha\in S(p')$ dunque, per definizione di
$stable(P)$, esiste $p''\in P$ tale che $p'' \wlred{\alpha}$.
%
Per concludere, dobbiamo dimostrare che $(P(\alpha), Q(\alpha)) \in {\rel{R}}$.
Ma
\[
  P(\alpha) = \{q\}(s)(\alpha) = \{q\}(s\alpha)
\]
per definizione di $P(\alpha)$ mentre
\[
  Q(\alpha) = \{(\{q\}(s), \acar{\mathcal{A}(\{q\}(s))})\}(\alpha) = \{(\{q\}(s\alpha), \acar{\mathcal{A}(\{q\}(s\alpha))})\}
\]
per costruzione dell'automa in forma normale ridotta e ora
\[
  \{(\{q\}(s\alpha), \{(\{q\}(s\alpha),\acar{\mathcal{A}(\{q\}(s\alpha))})\})\} \in {\rel{R}}
\]
per definizione di~$\rel{R}$.
\end{proof}

%\begin{figure}[h]
%  \centering
%    \includegraphics{examples/rnf.B.eps}
%  \caption{AC in f.n.r. dell'attivit\`a: $(a \oplus b)+(a \oplus c)$}
%  \label{fig:rnf_B}
%\end{figure}

\begin{example}
Dalla \figurename~\ref{fig:rnf_B} notiamo come l'automa sia diminuito consistentemente nel numero di stati rispetto a quello in  \figurename~\ref{fig:rnf_A} mantenendo sempre la stessa semantica, quindi i clienti soddisfatti di interagire con il servizio descritto in \figurename~\ref{fig:rnf_A}, lo saranno anche con quello in \figurename~\ref{fig:rnf_B}, che \`e computazionalmente (per numero di stati) meno oneroso del precedente. 
\end{example}
\begin{figure}[h]
  \centering
    \includegraphics{examples/rnf.B.eps}
  \caption{AC in f.n.r. dell'attivit\`a $(\co a \oplus \co b)+(\co a \oplus \co c)$}
  \label{fig:rnf_B}
\end{figure}
Da tale esempio possiamo affermare che l'intuizione sulla forma normale ridotta \`e giusta, nel senso che ci permette di effettuare una prima passata di minimizzazione dell'automa di origine, non in tutte le circostanze poich\'e a volte la normalizzazzione produce pi\`u stati rispetto all'automa originale e di ottenerne uno consono per la fase successiva di minimizzazione della forma normale ridotta. Abbiamo dato l'attributo di consono all'automa che scaturisce dalla normalizzazione poich\'e ci permette di applicare la tecnina classica di minimizzazione degli automi a stati finiti, ottenendo risultati veritieri che non avremmo ottenuto applicandola all'AC originale, come abbiamo gi\`a sottolineato in precedenza.

\section{Minimizzazione della forma normale ridotta}
Dopo aver definito la forma normale ridotta di un Automa Comportamentale, applichiamo ad essa la tecnica classica di minimizzazione che sulla base di un algoritmo ci permette di ricercare gli stati distinguibili, per un cliente, di un automa. \\
\label{sec:minimizzazione}
Dato un automa
\[
  N \eqdef (Q, \Sigma, \delta, q_0, F)
\]
in forma normale ridotta; diciamo che due stati $p,q\in Q$ sono \emph{indistinguibili} se soddisfano gli stessi clienti, quindi:
\[
 p \eqc q
\]
Se due stati  $p,q \in Q$ non sono \emph{indistinguibili} 
allora sono \emph{distinguibili}. Uno stato $p$ \`e \emph{distinguibile} da uno stato 
$q$ se esiste un cliente $c$ tale che $c \scomp p$ e $c \not\scomp q$ o viceversa.
\\
\\Definiamo ora un algoritmo per la ricerca degli stati distinguibili:
\\ 

\emph{base:} se $\mathcal{A}(p) \neq \mathcal{A}(q)$, allora $\{p,q\}$ \`e una \emph{coppia distinguibile}\\

\emph{induzione:} 
\begin{itemize}
\item due stati $p,q \in Q$ sono \emph{distinguibili} se esiste $p' \in \delta((p, \mathcal{A}), \tau)$
tali che per ogni $q'\in \delta((q, \mathcal{A}), \tau)$ abbiamo $\{p',q'\}$ \emph{distinguibile} e viceversa.
\item oppure se esiste un $\alpha\in\mathcal{A}$ tale che $\{p'\} = \delta'((p, \mathcal{A}),\alpha)$ ,
$\{q'\} = \delta'((q, \mathcal{A}),\alpha)$ e $\{p',q'\}$ \emph{distinguibile}.
\end{itemize}

\begin{theorem}(Correttezza)
Se due stati non sono distinti dall'algoritmo allora sono indistinguibili.
\end{theorem}
\begin{proof}
Assumiamo $N \eqdef (Q,\Sigma,\delta,q_0,F)$ 
essere un automa in forma normale ridotta sottoposto all'algoritmo per la ricerca delle coppie distinguibili e
supponiamo $\{p,q\}$ essere una coppia non distinta, ma $p$ e $q$ distinguibili, ovvero esiste
un cliente $r$ tale che :
\begin{enumerate}
\item $r \scomp p$ ma $r \not\scomp q$;

\item $r \not\scomp q$ implica $r \parop q \wlred{} r' \parop q' \nlred{}$ e $r'$ non finale.
\label{it:condizione2}
\end{enumerate}
Definiamo ogni $\{p,q\}$ che gode di queste due propriet\`a come una \emph{coppia cattiva}.
Tra tutte le \emph{coppie cattive} scegliamo $\{p,q\}$ come una coppia in cui $p$ e $q$ sono distinti
da un cliente $r$ per mezzo dell'interazione pi\`u corta.

Notiamo che l'interazione non pu\`o avere lunghezza pari a $0$ poich\`e deduciamo da $r \parop q \nlred{}$ che 
$r \nlred{}$ oppure se $r \lred{\alpha}$ implica $q \nlred{\alpha}$. Sappiamo che $\mathcal{A}(p) = \mathcal{A}(q)$
per cui $p \nlred{\alpha}$ e $r \parop p \nlred{}$ e $r$ deve essere finale dato che $r \scomp p$. 
Dalla condizione~\ref{it:condizione2} si nota che questo \`e un assurdo poich\`e $r$ non pu\`o essere finale.
Supponiamo allora che l'interazione abbia lunghezza $n>0$ quindi 
$r \parop q \lred{} r'' \parop q'' \wlred{} r' \parop q'\nlred{}$ dove possiamo distinguere tre casi:
\begin{itemize}
\item $(r \lred{\tau} r'', q = q'')$ allora $r \parop p \wlred{} r'' \parop p\nlred{}$ cio\`e
$r''$ distingue $p$ da $q$ con una interazione lunga $n-1$, ma questo \`e assurdo pioch\'e $\{p,q\}$ \`e
una coppia cattiva distinta da $r$ per mezzo dell'interazione pi\`u corta.
\item $(r = r'', q \lred{\tau} q'')$ sappiamo che $\mathcal{A}(p) = \mathcal{A}(q)$, siccome 
$\{p,q\}$ non sono stati distinti sappiamo che esiste $p''$ tale che $p \lred{\tau} p''$ e 
$\{p'',q''\}$ non sono distinguibili. Deduciamo per\`o dall'interazione che sono distinti da $r''$,
implicando che $\{p'',q''\}$ sia una coppia cattiva, ma cadiamo subito nell'assurdo per come abbiamo scelto $\{p,q\}$.
\item $(r \lred{\alpha} r'', q \lred{\alpha} q'')$ sappiamo che $\mathcal{A}(p) = \mathcal{A}(q)$
quindi abbiamo $p \lred{\alpha} p''$ dove $\{p,q\}$ non sono stati
distinti dall'algoritmo. Deduciamo per\`o dall'interazione che sono distinti da $r''$, implicando che $\{p'',q''\}$
sia una coppia cattiva, ma cadiamo subito nell'assurdo per come abbiamo scelto $\{p,q\}$.
\end{itemize}
\end{proof}

\begin{theorem}(Completezza) 
Se due stati sono indistinguibili allora non sono distinti all'algoritmo.
\end{theorem}
\begin{proof}
Supponiamo che esistano $p,q \in Q$ indistinguibili ma distinti dall'algoritmo al passo $n$.
Supponiamo inoltre che non ci siano altre coppie di stati indistinguibili ma distinti dall'algoritmo al passo $< n$,
ovvero tutte le coppie $\{p',q'\}$ distinte a passi $< n$ sono tali che $p'$ e $q'$ sono distinguibili.
Andiamo su $n$ per casi:
\begin{itemize}
\item $(n=0)$ Abbiamo che $\mathcal{A}(p)\neq \mathcal{A}(q)$ ma cadiamo nell'assurdo per definizione 
di stati indistinguibili. 
\item $(n>0)$ Esiste $p',q'$ tale che la coppia $\{p',q'\}$ \`e stata marcata distinguibile al passo $n-1$.
Allora $p'$ e $q'$ sono distinguibili ma allora esiste $\alpha\in\Sigma$ tale che $p\lred{\alpha}p'$ e $q\lred{\alpha}q'$
e cadiamo nell'assurdo poich\'e anche $p$ e $q$ sarebbero distinguibili.
\end{itemize}
\end{proof}
\newpage
La fase successiva alla verifica di completezza e correttezza dell'algoritmo di minimizzazione \`e la definizione formale dell'Automa Comportamentale in forma normale ridotta minimizzato, partendo dall'AC normalizzato e dalla notazione (Notazione \ref{not:class_eq}) di classe di equivalenza di uno stato.
\begin{notation}
\label{not:class_eq}
\[
	\lfloor p \rfloor = \{q\mid p \simeq q\}
\]
\end{notation}

Dato un automa
\[
	N \eqdef (Q, \Sigma, \delta, q_0, F)
\]
in forma normale ridotta, definiamo
\[
	M = (Q', \Sigma, \delta', \lfloor q_0 \rfloor, F')
\]
dove $Q'\subseteq 2^Q$ tale che
\[
\begin{array}{rcl}
  Q' & = & \{\lfloor p \rfloor \mid p \in Q\} 
\end{array}
\]
dove $\delta'$ \`e la pi\`u piccola funzione di transizione tale che
\[
\begin{array}{rcl}
  \delta'(P, \tau) & = & \{p' \mid \exists p \in P : \delta (p, \tau)\}
  \\
  \delta'(P, \alpha) & = & \{p' \mid \exists p \in P : \delta (p, \alpha)\}
\end{array}
\]
e
\[
\begin{array}{rcl}
	F' & = & \{\lfloor p \rfloor \mid p \in F\}
\end{array} 
\]
\\
\begin{example}
Consideriamo l'automa in \figurename~\ref{fig:rnf_B} e sottoponiamolo all'algoritmo per la ricerca degli stati distinguibili, vedi \tablename~\ref{tab:minimizzazione}. In \figurename~\ref{fig:rnf_C} notiamo che l'automa risultante dalla minimizzazione non \`e cambiato dal corrispettivo in forma normale ridotta poich\'e non sono stati trovati stati indistinguibili, vedi \tablename~\ref{tab:minimizzazione} dove tutte le coppie di stati sono marcate come distinguibili dall'algoritmo. 

\begin{table}[h]
\centering
\begin{tabular}{l|c|c|c|}
\cline{1-0} \cline{2-1}
$q_1$ & \ding{55}\\
\cline{1-0} \cline{2-1} \cline{3-2}
$q_2$ & \ding{55} & \ding{55} \\
\cline{1-0} \cline{2-1} \cline{3-2} \cline{4-3}
$q_3$ & \ding{55} & \ding{55} & \ding{55}\\
\hline
 & $q_0$ & $q_1$ & $q_2$\\
\end{tabular}
\caption{Ricerca degli stati distinguibili nell'AC in \figurename~\ref{fig:rnf_B}}
\label{tab:minimizzazione}
\end{table}

\begin{figure}[h]
  \centering
    \includegraphics{examples/rnf.C.eps}
  \caption{AC minimizzato dell'attivit\`a $(\co a \oplus \co b)+(\co a \oplus \co c)$}
  \label{fig:rnf_C}
\end{figure}
\end{example}
\newpage
Gli effetti di questa fase di minimizzazione sono palesi nell' esempio di \figurename~\ref{fig:minimizzazione} dove vengono rappresentati: l'automa originale (Figura~\ref{fig:min.A}), l'automa in forma normale ridotta (Figura~\ref{fig:min.B}) e l'automa in forma normale ridotta sottoposto alla minimizzazione (Figura~\ref{fig:min.C}). In questo esempio c'\`e da sottolineare l'aumento del numero di stati passando dall'automa originale all'automa in forma normale ridotta, ma siccome ci\`o che a noi interessa \`e l'AC finale che \`e diminuito (in numero di stati) rispetto all'originale, il fatto di avere un automa normalizzato pi\`u grande non induce problemi.
\begin{figure}[h]
\centering
\subfigure[AC\ originale \label{fig:min.A}]%
{\includegraphics[height=10.6cm]{examples/min.A.eps}}
\hspace{1cm}
\subfigure[AC\ in\ f.n.r \label{fig:min.B}]%
{\includegraphics[height=10.6cm]{examples/min.B.eps}}
\subfigure[AC\ minimizzato \label{fig:min.C}]%
{\includegraphics[height=10.9cm]{examples/min.C.eps}}
\caption{Minimizzazzione dell'AC del servizio Web $(\co a;(\co b \oplus c^\circledast))^\ast$}
\label{fig:minimizzazione}
\end{figure}

